The Runtime Complexity (full) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

Rewrite Strategy: FULL

(1) CpxTrsToCpxRelTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to relative TRS where S is empty.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s(X), incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s(X)) → s(X)
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

S is empty.
Rewrite Strategy: FULL

(3) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
s/0

(4) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

a__nats → a__adx(a__zeros)
a__zeros → cons(0, zeros)
a__incr(cons(X, Y)) → cons(s, incr(Y))
a__adx(cons(X, Y)) → a__incr(cons(X, adx(Y)))
a__hd(cons(X, Y)) → mark(X)
a__tl(cons(X, Y)) → mark(Y)
mark(nats) → a__nats
mark(adx(X)) → a__adx(mark(X))
mark(zeros) → a__zeros
mark(incr(X)) → a__incr(mark(X))
mark(hd(X)) → a__hd(mark(X))
mark(tl(X)) → a__tl(mark(X))
mark(cons(X1, X2)) → cons(X1, X2)
mark(0) → 0
mark(s) → s
a__nats → nats
a__adx(X) → adx(X)
a__zeros → zeros
a__incr(X) → incr(X)
a__hd(X) → hd(X)
a__tl(X) → tl(X)

S is empty.
Rewrite Strategy: FULL

(5) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
a__hd(cons(hd(cons(X1985_3, X2986_3)), Y)) →⁺ a__hd(cons(X1985_3, X2986_3))
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [X1985_3 / hd(cons(X1985_3, X2986_3))].
The result substitution is [Y / X2986_3].

(6) BOUNDS(n^1, INF)